/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

/* Message from Xiaoming Li and Darko Marinov, May 2005:
     To use logging, all you need to do is set the logging parameter
     to "Always" or "Ask" using "-Dalloy.logging" property or preferences.
     For example, for jar version:
       java -Dalloy.logging=Always -jar alloy.jar
*/

package alloy.api;

import java.io.File;
import java.io.FileOutputStream;
import java.io.InputStream;
import java.io.PrintWriter;
import java.io.Reader;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.ast.Command;
import alloy.ast.Commands;
import alloy.ast.DummyNode;
import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.LeafId;
import alloy.ast.Location;
import alloy.ast.Node;
import alloy.ast.Specification;
import alloy.bool.BLBackend;
import alloy.bool.BoolStencil;
import alloy.bool.BooleanFormula;
import alloy.log.AlloyLog;
import alloy.parse.visitor.MakeASTVisitor;
import alloy.semantic.ClosedTypesDetectionVisitor;
import alloy.semantic.CommandVisitor;
import alloy.semantic.ConstructExtendsGraphVisitor;
import alloy.semantic.FieldTypeChecker;
import alloy.semantic.FormulaTypeCheckVisitor;
import alloy.semantic.FunctionArgTypeCheckVisitor;
import alloy.semantic.MakeModuleScopesVisitor;
import alloy.semantic.NoParagraphNameShadowingVisitor;
import alloy.semantic.SigTypeCreator;
import alloy.semantic.SignatureReferenceCounter;
import alloy.sharbool.TemplateDetectVisitor;
import alloy.symm.SymmetryBreaker;
import alloy.transform.ConstructInvocationGraphVisitor;
import alloy.transform.DesugarIntExprCastExprVisitor;
import alloy.transform.DesugarLetVisitor;
import alloy.transform.DesugarRestrictionVisitor;
import alloy.transform.DesugarSumExprVisitor;
import alloy.transform.FunctionSkolemizer;
import alloy.transform.GenCommandFormulasVisitor;
import alloy.transform.IntCastRemovalVisitor;
import alloy.transform.InvocationInlineVisitor;
import alloy.transform.RenameQuantifiedVarsVisitor;
import alloy.transform.SetLeafIdsVisitor;
import alloy.transform.SkolemizationVisitor;
import alloy.transform.atomize.AtomizationState;
import alloy.transform.atomize.AtomizationVisitor;
import alloy.transform.atomize.AtomizePrePass;
import alloy.transl.ASTInfoVisitor;
import alloy.transl.BoolVarAllocator;
import alloy.transl.DefaultRelationAllocator;
import alloy.transl.ExprTransl;
import alloy.transl.FormulaTransl;
import alloy.transl.RelationAllocator;
import alloy.transl.Transl;
import alloy.transl.TranslException;
import alloy.transl.TranslInfo;
import alloy.transl.TranslVisitor;
import alloy.type.BasicType;
import alloy.type.ScopedType;
import alloy.type.SigType;
import alloy.util.CleanupManager;
import alloy.util.Dbg;
import alloy.util.EnvFailureException;
import alloy.util.FileUtil;
import alloy.util.Msg;
import alloy.util.Params;
import alloy.util.SetOfLong;
import alloy.util.TmpFiles;
import alloy.viz.alloyviz.MetamodelGenerator;

/**
 * Provides a complete programmatic interface for running the Alloy
 * analyzer on a specification.  Given Alloy spec in
 * files on disc, you can run Alloy analyses by calling
 * static methods of this class.  Results of each analysis
 * are returned in a programmatic data structure,
 * {@link SolutionData}.
 * <p>
 * Since static methods and fields are used this code is non-reentrant i.e.
 * it should only be used from one place.  After finishing
 * one analysis, you can run another using the same methods
 * from this class.
 * <p>
 * Note that the Alloy spec which we analyze, and all specs it
 * references, must be in files on disk, not in memory.
 * This is because specs can reference other specs via
 * <code>open</code> and <code>uses</code> clauses,
 * and the referencing is done by referencing file names.
 * This can be a nuisance for people who automatically generate
 * specs, or for the GUI where the user has typed a spec but
 * has not yet saved it.  Eventually, at least the main spec file,
 * on which the analysis starts, will be allowed to reside in memory.
 * For now, all .als files must reside on disc.
 * <p>
 * All randomness used in the analysis is controlled by one random
 * seed set at the beginning of the analysis.  So results can be
 * completely reproduced if the same random seed is used.
 * <p>
 * This programmatic interface is used by Alloy's command-line interface
 * {@link alloy.cli} as well as by the GUI interface {@link alloy.gui.NewAlloyGUI}.
 * <p>
 * To do an analysis, you first call {@link #prepareSpec}
 * with a filename of the main .als spec (which may
 * open or use other specs as needed).  If it returns
 * <code>true</code> indicating no syntax errors,
 * you can start analyzing any run/check/eval {@link Command}s in the spec.
 * {@link #getCommands} returns the available {@link Command}s.
 * You then call {@link #translateCommand} on the command, which constructs a
 * Boolean translation of the command; it returns a {@link SolutionData} object
 * containing information about the Alloy formula and its Boolean translation, as well
 * as a a blank solution (all relations having empty tuple sets).
 * You then pass this to {@link #analyzeCommand} which runs the alloy analysis by
 * finding a solution satisfying the Alloy formula, and returns the results in a new {@link SolutionData} object.
 * {@link #getNextSolution} will search for another solution to the
 * last analyzed command.  The reason you first call {@link #translateCommand} to get a "blank" solution
 * is that we also have an enter-an-instance mode where the user enters a solution by hand and then
 * sees which parts of the formula that solution satisfies; for that mode you just use {@link #translateCommand}
 * without calling {@link #analyzeCommand}.  But for normal Alloy analyses, you call {@link #translateCommand} then
 * take the blank {@link #SolutionData} it returned and pass it to {@link #analyzeCommand} which does the
 * analysis.  See {@link alloy.cli.AlloyCLI#_runCommand} for examples of usage of this API.
 * <p>
 * You can also get a {@link String} describing a given {@link SolutionData instance};
 * see {@link #instance2alloyFunction}.
 */
public final class AlloyRunner {

    /** Alloy specification to analyze */
    private static Specification _spec;

    private static FunctionSkolemizer _fs;

    /** most recent translator */
    private static TranslInfo _translator;

    /** most recent boolean formula */
    private static BooleanFormula _translation;

    /** most recent symmetry-breaking predicate */
    private static BooleanFormula _symmBrkPredicate;

    /** most recent Alloy formula that we analyzed */
    private static Formula _formulaToAnalyze;

    /** most recent Alloy formula that we showed in the alloy evaluator window */
    private static Formula _formulaToView;

    /** Last translated command. */
    private static Command _lastTranslatedCommand;

    /**
     * Last template detect visitor, if in use.  Saved here so we can tell it to interrupt
     * analysis if needed.
     */
    private static TemplateDetectVisitor _lastTemplateDetector;

    /** Flag indicating if the last analysis attempt succeeded **/
    private static boolean _lastAnalysisSucceeded;

    /** Whether the user has told us to interrupt analysis. */
    private static boolean _interruptInProgress;

    /** Check the environment to make sure all the necessary files
    are present, the temporary directory is writeable, etc.
    If there is a problem, returns a {@link String} error message;
    otherwise returns <code>null</code>. */
    public static String checkEnvironment() {
        return BLBackend.checkEnvironment();
    }

    /** Reset all state to its initiali value. */
    public static void clearState() {
        _formulaToAnalyze = null;
        _formulaToView = null;
        _fs = null;
        _interruptInProgress = false;
		_lastAnalysisSucceeded = true;
        _lastTranslatedCommand = null;
        _spec = null;
        _symmBrkPredicate = null;
        _translation = null;
        _translator = null;

        gc();
        
		SetLeafIdsVisitor.clearState();
		SkolemizationVisitor.clearState();
		BooleanFormula.initSingletons();
		FormulaTransl.initSingletons();
		SigType.init();
		AtomizationState.init();

        gc();
    }

    private static void gc() {
    	for (int i=5; i>0; i--) {
    		System.gc();
    	}
    }
    
    
    /**
     * Whether the solver currently selected by global parameters is capable of
     * enumerating solutions.
     */
    public static boolean enumeratingSolverSelected() {
        return BLBackend.canEnumerateSolutions(Params.glob.getParam("MAIN","solver"));
    }

    /** Whether the given solver can enumerate solutions */
    public static boolean canEnumerateSolutions(String solverName_) {
        return BLBackend.canEnumerateSolutions(solverName_);
    }

    /**
     * Parse, check for semantic correctness, and desugar an
     * Alloy specification, preparing it for analysis.  This
     * spec can then be analyzed by calling {@link #analyzeCommand}.
     * <p>
     * Utilizes the value of {@link #skolemInsideUniv} flag to
     * decide whether to skolemize inside universal quantifiers.
     *
     * @param filename_ the name of the file containing the
     * main module of the specification
     * @return <code>true</code> if the specification passed
     * all syntactic and semantic checks; <code>false</code>
     * otherwise.  Error messages should be handled through an
     * {@link alloy.util.Dbg.DbgMsgListener}.
     */
    public static boolean prepareSpec(String filename_) {
        if (filename_ == null) return false;

        AlloyLog.logStartSession(AlloyLog.BUILD);

        _initForNewSpec();
        File file = new File(filename_);
        if (!file.isFile()) {
            Dbg.user(new Msg("File " + filename_ + " not found.", new DummyNode()));
            return false;
        }
        _spec = MakeASTVisitor.getAST(file);


    //for (Iterator modIter = _spec.getModules().getModuleIter(); modIter.hasNext();) {
    //    System.out.println("_spec mod " + modIter.next());
    //}

        //System.out.println("About to finish preparation in prepareSpec(String filename)");
        return _finishPreparation(null);
        
    }

    /**
     * Finishes preparation of a spec.  Assumes that
     * {@link MakeASTVisitor#getAST(String)} or
     * {@link MakeASTVisitor#getAST(InputStream)} has
     * already been called.
     */
    private static boolean _finishPreparation(String specString_) {
        if (Dbg.userError || (_spec == null)) {
            AlloyLog.logBuild(_spec, specString_);
            AlloyLog.logEndSession(AlloyLog.BUILD);
            return false;
        }
        //Dbg.info(ExprTypeCheckVisitor.moduleScopes.toString());
        //System.out.println("performing semantic checks");
        long start, end;
        
        start = System.currentTimeMillis();
        _performSemanticChecks();
        end = System.currentTimeMillis();
        Dbg.info("Performed semantic checks (" + ((end - start)/1000.00) + "s)" );
        //System.out.println("performed semantic checks");
        if (Dbg.userError) {
            AlloyLog.logBuild(_spec, specString_);
            AlloyLog.logEndSession(AlloyLog.BUILD);
            return false;
        }

        //System.out.println("performing elaborations");
        start = System.currentTimeMillis();
        _performElaborations();
        end = System.currentTimeMillis();
        Dbg.info("Performed elaborations (" + ((end - start)/1000.00) + "s)" );
        //System.out.println("performed elaborations");
        if (Dbg.userError) {
            AlloyLog.logBuild(_spec, specString_);
            AlloyLog.logEndSession(AlloyLog.BUILD);
            return false;
        }

        AlloyLog.logBuild(_spec, specString_);
        AlloyLog.logEndSession(AlloyLog.BUILD);
        return true;
    }

    /**
     * Initialize program state to handle a new spec.
     */
    private static void _initForNewSpec() {
        // Clear the record of files and objects to be dumped
        // in case an internal error is encountered.
        Dbg.clearDump();
        // set skolemization flag
        alloy.transform.SkolemizationVisitor.maxSkolDepth = Params.glob.getIntParam("MAIN", "skoldepth");
        // clear error flag
        Dbg.userError = false;
            //We don't need this anymore? ImplicitConstraintGenerator.init();
        // initialize module paths
        FileUtil.setModulePath(Params.glob.getPathParam("MAIN", "modulePath"));
        // essential to avoid memory leak
        clearState();
    }

    /**
       <p>Parse, check for semantic correctness, and desugar an
       Alloy specification, preparing it for analysis.  This
       spec can then be analyzed by calling {@link #analyzeCommand}.
       <p>Utilizes the value of {@link #skolemInsideUniv} flag to
       decide whether to skolemize inside universal quantifiers.
      @param specString_ the String containing the main
       module of the specification.  Note that {@link alloy.ast.Location}s
       for {@link alloy.ast.Node}s in the main module will have
       file name {@link alloy.ast.Location#NOT_FROM_FILE}.
       @return <code>true</code> if the specification passed
       all syntactic and semantic checks; <code>false</code>
       otherwise.  Error messages should be handled through an
       {@link alloy.util.Dbg.DbgMsgListener}.
    */
    public static boolean prepareSpecString(String specString_) {
        if (specString_ == null) return false;

        AlloyLog.logStartSession(AlloyLog.BUILD);

        _initForNewSpec();
        _spec = MakeASTVisitor.getAST(Location.NOT_FROM_FILE, specString_);
        //System.out.println("About to finish preparation in prepareSpecString");
        return _finishPreparation(specString_);
    }

    /**
       <p>Parse, check for semantic correctness, and desugar an
       Alloy specification, preparing it for analysis.  This
       spec can then be analyzed by calling {@link #analyzeCommand}.
       <p>Utilizes the value of {@link #skolemInsideUniv} flag to
       decide whether to skolemize inside universal quantifiers.
      @param reader_ the Reader containing the main
       module of the specification.  Note that {@link alloy.ast.Location}s
       for {@link alloy.ast.Node}s in the main module will have
       file name {@link alloy.ast.Location#NOT_FROM_FILE}.
       @return <code>true</code> if the specification passed
       all syntactic and semantic checks; <code>false</code>
       otherwise.  Error messages should be handled through an
       {@link alloy.util.Dbg.DbgMsgListener}.
    */
    public static boolean prepareSpec(Reader reader_) {
        if (reader_ == null) return false;

        AlloyLog.logStartSession(AlloyLog.BUILD);

        _initForNewSpec();
        _spec = MakeASTVisitor.getAST(Location.NOT_FROM_FILE, reader_);
        //System.out.println("About to finish preparation in prepareSpec");
        return _finishPreparation(null/* it seems that prepareSpec(Reader) is never used*/);
    }

    /** @return the commands of the current spec, or <code>null</code> if
        there is no current spec */
    public static Commands getCommands() {
        if (_spec == null) return null;
        return _spec.getFocus().getCommands();
    }

    /** Get the next solution for the most recently analyzed command.
        Note that {@link #multipleSolutions} must have been set to
        <code>true</code> when the command was originally analyzed for
        this method to work properly.
        @return the next solution, or <code>null</code> if there are no
        more solutions
    */
    public static SolutionData getNextSolution() {
        if (_translation == null || _translator == null) return null;
        SolutionData ret = null;
        int solveResult = BLBackend.next();
        if (solveResult == BLBackend.BL_SAT) {
            boolean[] lastSol = BLBackend.getLastSolution();
            Dbg.chk(lastSol);
        if (!Boolean.getBoolean("alloy.nochk"))
        Dbg.chk(_translation.interpret(lastSol));

            ret = new Instance(_translator, lastSol, _formulaToAnalyze, _lastTranslatedCommand,
                       _translation, _spec, _fs);
        ret.setVizInstance(ret.getVizInstance());
        }
        return ret;
    }

    /** Interrupt the currently running analysis, causing it to return immediately
    with a "no solutions" finding. */
    public static void interruptAnalysis() {
	_interruptInProgress = true;
	if (_lastTemplateDetector != null)
	    _lastTemplateDetector.interrupt();
        BLBackend.getInstance().interruptSolver();
    }

    /** Given a {@link SolutionData} and a modified boolean assignment,
    returns a new {@link SolutionData} with the new boolean assignment.
    Used by the Alloy Evaluator functionality: the user edits the
    bits of the given instance. */
    public static SolutionData getModifiedSolution(SolutionData originalSolution_,
                           boolean[] newAssignment_) {
    Dbg.chk(newAssignment_.length == originalSolution_.getSolution().length);

    // experimental functionality added by DNJ

    SolutionData solData = new Instance(originalSolution_.getTranslator(),
                    newAssignment_,
                    originalSolution_.getFormula(),
                    originalSolution_.getCommand(),
                    originalSolution_.getTranslation(),
                    originalSolution_.getSpecification(),
                    originalSolution_.getSkolemizer());

    solData.setVizInstance(solData.getVizInstance());
    return solData;
    }

    /** described in file alloy2/alloy/semantic/README */
    private static void _performSemanticChecks() {
		MakeModuleScopesVisitor mmsv = new MakeModuleScopesVisitor();
		_spec.applyVisitor(mmsv);
		if (Dbg.userError) return;
		NoParagraphNameShadowingVisitor npnsv = new NoParagraphNameShadowingVisitor();
		_spec.applyVisitor(npnsv);
		if (Dbg.userError) return;

		ConstructExtendsGraphVisitor cegv = new ConstructExtendsGraphVisitor();
		//  Dbg.info(_spec.getModules().toString());
		_spec.applyVisitor(cegv);
		if (Dbg.userError) return;
		List sortedSigs = cegv.getSortedSigs();

		SigTypeCreator.createSigTypes(sortedSigs, _spec.getFocus()
				.getModuleInfo());

		/***********************************************************************
		 * NOTE: let desugaring is now done after all the typechecking, since
		 * since expressions assigned to let variables need to be typechecked as
		 * well.
		 **********************************************************************/

		if (Dbg.userError) return;

		//System.out.println("____________FieldTypeChecker____________");
		FieldTypeChecker.typecheckFields(sortedSigs);

		if (Dbg.userError) return;

		//System.out.println("____________FunctionArgTypeCheckVisitor____________");
		_spec.applyReturnVisitor(new FunctionArgTypeCheckVisitor());

		if (Dbg.userError) return;

		//System.out.println("____________FormulaTypeCheckVisitor____________");
		_spec.applyVisitor(new FormulaTypeCheckVisitor());

		if (Dbg.userError) return;
	}

    /** @see alloy.transform */
    private static void _performElaborations() {
     
	_spec.applyReturnVisitor(new DesugarLetVisitor());
	
    //System.out.println("____________RenameQuantifiedVarsVisitor____________");
    _spec.applyReturnVisitor(new RenameQuantifiedVarsVisitor());

    //System.out.println("____________DesugarRestrictionVisitor____________");
    _spec.applyReturnVisitor(new DesugarRestrictionVisitor());

    //System.out.println("____________DesugarSumExprVisitor____________");
    _spec.applyReturnVisitor(new DesugarSumExprVisitor());

    //System.out.println("____________ConstructInvocationGraphVisitor____________");
        ConstructInvocationGraphVisitor cigv = new ConstructInvocationGraphVisitor();
        _spec.applyVisitor(cigv);

    if (Dbg.userError) return;

    //We don't want to deal with recursion yet.
    _fs = new FunctionSkolemizer();
    /**
    for (Iterator iter = cigv.getRecursiveInvocables().iterator();
             iter.hasNext(); ) {
        _fs.skolemizeFunction((InvocablePara)iter.next());
    }
    **/

    List sortedFunctions = cigv.getSortedInvocables();

    //System.out.println("____________InvocationInlineVisitor____________");

        InvocationInlineVisitor.inlineFunctionBodyInvocations(sortedFunctions,_fs);
    
    if (Dbg.userError) return;

    _spec.applyReturnVisitor(new InvocationInlineVisitor(_fs));
    
    if (Dbg.userError) return;

    //System.out.println("____________IntCastRemovalVisitor____________");
    _spec.applyReturnVisitor(new IntCastRemovalVisitor());
    if (Dbg.userError) return;
    
    _spec.applyReturnVisitor(new DesugarIntExprCastExprVisitor());
    if (Dbg.userError) return;

    //System.out.println("____________GenCommandFormulasVisitor____________");
    _spec.applyVisitor(new GenCommandFormulasVisitor());
    if (Dbg.userError) return;

    //System.out.println("____________CommandVisitor____________");
    _spec.applyVisitor(new CommandVisitor());
    if (Dbg.userError) return;
    
    /**
    System.out.println("COMMANDS BEFORE ATOMIZATION: ");
    for (Iterator commandIter = _spec.getFocus().getCommands().getCommandIter();
	 commandIter.hasNext();) {
	FindCommand command = (FindCommand) commandIter.next();
	System.out.print(command.nodeString()  + " : " );
	System.out.println(command.formula.pp());
    }
    */

    //System.out.println("**********Unmapped leaves after TypeChecking**********");
    //getCommands().applyVisitor(new alloy.semantic.LeafIdToMultCheckVisitor());

    //System.out.println("____________ClosedTypesDetectionVisitor____________");
    _spec.getFocus().applyVisitor(new ClosedTypesDetectionVisitor());
    if (Dbg.userError) return;
  
    
    // counts the times each signature is referenced in field declarations
    _spec.getFocus().applyVisitor(new SignatureReferenceCounter());
    
    // Just-In-Time atomization will only process the Specification and Module object but 
    // not individual commands.  The atomizaiton of individual commands is done in 
    // the beginning of translateCommand.
    //System.out.println("____________AtomizationVisitor____________");
    _spec.applyReturnVisitor(new AtomizePrePass());

    /**
    System.out.println("COMMANDS AFTER ATOMIZATION: ");
    for (Iterator commandIter = _spec.getFocus().getCommands().getCommandIter();
     commandIter.hasNext();) {
    FindCommand command = (FindCommand) commandIter.next();
    System.out.print(command.nodeString()  + " : " );
    System.out.println(command.formula.pp());
    } 
    **/

    //System.out.println("**********Unmapped leaves after Atomization**********");
    //getCommands().applyVisitor(new alloy.semantic.LeafIdToMultCheckVisitor());
    }

    public static alloy.viz.alloyviz.VizInstance metamodel() {
        if (_spec==null) {
            return null;
        }
        else {
            MetamodelGenerator mg = new MetamodelGenerator(_spec);
            return mg.getInstance();
        }
    }

    /**
     * Translate the formula for the given {@link Command} into a {@link BooleanFormula},
     * but do not execute the solver.  This is used by Alloy Evaluator: instead of solving
     * the formula for a satisfying instance, we ask the user to enter an instance.
     *
     * @return {@link SolutionData} with all Boolean variables set to false, or null if {@link #interruptAnalysis}
     *   is called during translation.
     * @throws {@link TranslationException} if command cannot be translated due to lack of resources
     *         (e.g. memory) or due to limitations of the current translator implementation
     */
    public static SolutionData translateCommand(Command command_) throws TranslationException {
        //System.out.print(((FindCommand)command_).nodeString()  + " : " );
        //System.out.println(((FindCommand)command_).formula.pp());

        AlloyLog.logStartSession(AlloyLog.COMMAND);

	_interruptInProgress = false;
        
	AtomizationVisitor.atomize( (FindCommand)command_ );

	if (_interruptInProgress) return null;
    
        
        _formulaToAnalyze = _formulaToView = ((FindCommand)command_).formula;

       //System.out.println(_formulaToAnalyze.nodeString() + " : ");
       //System.out.println(_formulaToAnalyze.pp());
        
        //Dbg.info(alloy.type.SigType.getSigTypeStrings().toString());
        //alloy.RunAlloy.viewTree(findCommand.formula, "command formula", null, null, null, null);

        //System.out.println("In translateCommand: "+ _formulaToAnalyze.nodeString());
        // ^^^ feel free to uncomment if still needed

        ScopedType.setBasicTypeScopes(command_);

        // Check that the translatable AST is well-formed
        //_formulaToAnalyze.applyVisitor(new TranslatableASTCheckVisitor());

        // Gather various information about the translatable AST, and store it all
        // in one object implementing the ASTInfo interface

        ASTInfoVisitor astInfoVisitor = new ASTInfoVisitor((FindCommand)command_);
        _formulaToAnalyze.applyVisitor(astInfoVisitor);

	if (_interruptInProgress) return null;
	
        // Allocate Boolean variables to relations
        BoolVarAllocator boolVarAlloc = new BoolVarAllocator();

        RelationAllocator relationAlloc =
        		new DefaultRelationAllocator(astInfoVisitor, boolVarAlloc, command_.intWidth);

        boolean useSymm = Params.glob.getBoolParam("MAIN", "usesymm");
        SymmetryBreaker symmetryBreaker = null;
        if (useSymm) {
            symmetryBreaker = new SymmetryBreaker(astInfoVisitor, relationAlloc);
            symmetryBreaker.breakSymmsBeforeTranslation(((FindCommand)command_).scopedSigsInfo,
                                command_.leafId2Scope,
                                ((FindCommand)command_).id2Annotation);
        }

	if (_interruptInProgress) return null;

        // Translate Alloy formula to Boolean formula; this may throw a TranslException
        try { _translator = TranslVisitor.translate(_formulaToAnalyze, astInfoVisitor, relationAlloc); }
        catch (TranslException te_) { throw new TranslationException(te_.toString()); }
	
	if (_interruptInProgress) return null;

    if (useSymm) {
			symmetryBreaker.breakSymmsAfterTranslation(_translator);
			_symmBrkPredicate = symmetryBreaker.getSymmetryBreakingPredicate();
		}
	if (_interruptInProgress) return null;

    //System.out.println("full formula: " + _formulaToAnalyze.getNode().replacednodeString());
	FormulaTransl formulaTransl = (FormulaTransl) _translator.getNodeTransl(_formulaToAnalyze);
	//Dbg.info(_translator.getBasicTypes().toString());
	_translation = formulaTransl.formula.and(boolVarAlloc.getVarConstraints());
	boolean[] solution = new boolean[boolVarAlloc.getNumAllocatedVars() + 1];
	alloy.type.SigType.computeShortSigNames(_translator.getBasicTypes());

        SolutionData ret =
        		new Instance(_translator,
        					solution,
						_formulaToView,
						_lastTranslatedCommand = command_,
						_translation,
						_spec,
						_fs);
        ret.setVizInstance(ret.getVizInstance());

        AlloyLog.logCommand(command_);
        AlloyLog.logEndSession(AlloyLog.COMMAND);

        return ret;
    }  // translateCommand()

    /** Run the actual Alloy analysis on a given {@link Command}: gather the Alloy
    {@link Formula} specified by the command, desugar it, translate into a
    {@link BooleanFormula}, run SAT solver to find a solution to the
    {@link BooleanFormula}, interpret the solution to produce a
    {@link SolutionData} result object.  */
    public static SolutionData analyzeCommand(SolutionData solData_, long randSeed_) throws EnvFailureException {
        return analyzeCommand(solData_, randSeed_, null /* primaryRelationIds_ */);
    }

    /** Run the actual Alloy analysis on a given {@link Command}: gather the Alloy
    {@link Formula} specified by the command, desugar it, translate into a
    {@link BooleanFormula}, run SAT solver to find a solution to the
    {@link BooleanFormula}, interpret the solution to produce a
    {@link SolutionData} result object.
    Returns null if {@link #interruptAnalysis} is called during analysis.
    */
    public static SolutionData analyzeCommand(SolutionData solData_, long randSeed_,
                          Set primaryRelationIds_) throws EnvFailureException {
	if (_interruptInProgress) return null;
        randSeed_ = Params.glob.getLongParam("MAIN", "randseed");

        // record the random seed in case of error, so we can reproduce the analysis
        Dbg.addObjToDump("Random seed: ", new Long(randSeed_));

        _translator = solData_.getTranslator();
        _formulaToAnalyze = solData_.getFormula();

        BoolVarAllocator boolVarAlloc = _translator.getBoolVarAllocator();
        int nvars = boolVarAlloc.getNumAllocatedVars();
        Dbg.info(nvars + " bits of state.");
        RelationAllocator relationAlloc = _translator.getRelationAllocator();

        //
        // Perform optional optimizations: if they fail for some reason
        // (bug in the code), we can still do the analysis -- it just won't be
        // as efficient.
        //

        //
        // Detect shared Boolean subformulas, to reduce the size of the final CNF
        // formula that we output
        //
        if (Params.glob.getBoolParam("MAIN","sharbool")) {
            try {
            TemplateDetectVisitor templateDetector = new TemplateDetectVisitor(_translator);
	    _lastTemplateDetector = templateDetector;
            templateDetector.preprocess(_formulaToAnalyze);
            _formulaToAnalyze.applyReturnVisitor(templateDetector);
            templateDetector.postprocess();
            //templateDetector.showTemplates();
            
            // clear unnecessary data to reduce memory drag
            _lastTemplateDetector = null;
            
            } catch (Exception e_) { Dbg.warn("Template detection failed", e_); }
        }
	if (_interruptInProgress) return null;

		Dbg.chk(_translation != null, "translation is null in AlloyRunner.analyzeCommand()");
		
        if (Params.glob.getBoolParam("MAIN", "usesymm")) {
            _translation = _translation.and(_symmBrkPredicate);
        }

        //
        // If primary relations are defined, write their variables to a file.
        //
        File primVarFileHandle = null;
        if (primaryRelationIds_ != null) {
            PrintWriter w = null;
            try {
                primVarFileHandle = TmpFiles.createHandleToATempFile("primvars.dat");
                w = new PrintWriter(new FileOutputStream(primVarFileHandle));
                for (Iterator primIdIter = primaryRelationIds_.iterator(); primIdIter.hasNext();) {
                    LeafId primRelId = (LeafId)primIdIter.next();
                    ExprTransl exprTransl = (ExprTransl)_translator.getLeafTransl(primRelId);
                    for (Iterator boolFormIter = exprTransl.getBooleanFormulas().iterator(); boolFormIter.hasNext();) {
                        BooleanFormula f = (BooleanFormula)boolFormIter.next();
                        if (f.isLiteral()) {
                            int lit = f.getLiteral();
                            w.println(Math.abs(lit));
                        }
                    }
                }
                w.println(0);
            } catch (Exception e_) {
                Dbg.info("primVar file could not be created: " + e_);
                primVarFileHandle = null;
            } finally {
                if (w != null) w.close();
            }
        }
        //Dbg.info("primaryRelationIds: " + primaryRelationIds_);
        //Dbg.info("primVarFileName: " + primVarFileHandle);

        //
        // Solve the Boolean formula.
        //
        int solveResult;

	if (_interruptInProgress) return null;
        long start = System.currentTimeMillis();
        
	// DON'T CATCH THE ENV_FAILURE_EXCEPTION
	// AND LET THE GUI HANDLE IT
	/**
        try {
            solveResult = BLBackend.solve(_translation,  nvars, null,  // dependentVars_
                          Params.glob.getParam("MAIN", "solver"),
                          Params.glob.getBoolParam("MAIN", "multsol") ?
                          BLBackend.ENUM_ON : BLBackend.ENUM_OFF,
                          randSeed_, BLBackend.BL_RUN_SOLVE,
                          primVarFileHandle);
        } catch (EnvFailureException e_) {
            //throw new Error("Env failure");
        }
	**/
	solveResult = BLBackend.solve(_translation,  nvars, null,  // dependentVars_
				      Params.glob.getParam("MAIN", "solver"),
				      Params.glob.getBoolParam("MAIN", "multsol") ?
				      BLBackend.ENUM_ON : BLBackend.ENUM_OFF,
				      randSeed_, BLBackend.BL_RUN_SOLVE,
				      primVarFileHandle);

        long finish = System.currentTimeMillis();
                
        if (solveResult == BLBackend.BL_SAT) {
            boolean[] lastSol = BLBackend.getLastSolution();
            Dbg.chk(lastSol);
            if (!Boolean.getBoolean("alloy.nochk"))
            Dbg.chk(_translation.interpret(lastSol));
            //System.out.println(_translation.interpret(lastSol));
            //SolutionData modSol = getModifiedSolution(solData_, lastSol);
            //System.out.println("Solution: " + modSol);
            return getModifiedSolution(solData_, lastSol);
        } else 
            // formula not satisfiable -- no solution
	    // AlloyRunner.computeLiftedUnsatCore();
	    //System.out.println("Formula not satisfiable or an error occurred");
            return null;
    }  // analyzeCommand

    /**
     * Compute the unsatisfiable core of the last analyzed formula (assumed to be
     * unsatisfiable).
     * @see LiftedUnsatCore
     * @todo what happens if the unsat core computation fails?
     */
    public static LiftedUnsatCore computeLiftedUnsatCore() {
	final BoolStencil groundUnsatCore = BLBackend.computeUnsatCore();

	return new LiftedUnsatCore() {
			public boolean isInCore(Node node_) {
				final Transl nodeTransl = _translator.getNodeTransl(node_);
				if (nodeTransl == null)
					return true; // be conservative (?)
				for (Iterator boolFormulas = nodeTransl.getBooleanFormulas().iterator(); boolFormulas.hasNext();) {
					final BooleanFormula bf = (BooleanFormula) boolFormulas.next();
					if (groundUnsatCore.allowsLifted(bf)) //this is the key call
						return true;
				}
				return false;
			}

			//TODO not sure this is right
			public SetOfLong nodeTemplates (final Node node_) {
				final Transl nodeTransl = _translator.getNodeTransl(node_);
				final SetOfLong templates = new SetOfLong();
				if (nodeTransl != null) {
					for (Iterator boolFormulas = nodeTransl.getBooleanFormulas().iterator(); boolFormulas.hasNext();) {
						final BooleanFormula bf = (BooleanFormula) boolFormulas.next();
						//accumulator
						templates.addAll(groundUnsatCore.BfTemplates(bf)); //this is the key call
					}
				}
				return templates;
			}
		};
	}
    

    /**
	 * Return a description of the last instance returned, as a {@link String}
	 * of Alloy: the string contains a predicate without arguments, named
	 * InstanceNN where NN is incremented for each call, which will force an
	 * instance isomorphic to the last instance to be returned. The GUI has a
	 * command to paste the returned predicate into the spec, for use with Alloy
	 * Evaluator (to see why this instance is excluded by some modification of
	 * the constraints), or for "regression testing" of your spec (to make sure
	 * that future constraints you write do not accidentally disallow this
	 * instance.)
	 * <p>
	 * Implementation: the function we generate has the form
	 * pred Instance1 ( ) {
	 * some disj A0, A1: A, disj B0, B1: B | {
	 * A$p = A0->B0 + A1->B1
	 * B$q = B0->B0 + B1->B1
	 * }
	 *
	 * if we had
	 * sig A { p: set B }
	 * sig B { q: set B }
     */
    public static String instance2alloyPredicate(SolutionData instance_) {
		StringBuffer alloyFunction = new StringBuffer();
		alloyFunction.append("pred Instance ( ) { some ");
		for (Iterator basicTypeIter = instance_.allTypes().iterator(); basicTypeIter.hasNext();) {
			BasicType basicType = (BasicType) basicTypeIter.next();
			String sigName = basicType.toString();
			List atomList = instance_.atomsOfSig(sigName);
			if (!atomList.isEmpty()) {
				if (atomList.size() > 1)
					alloyFunction.append(" disj ");
				for (Iterator atomIter = atomList.iterator(); atomIter.hasNext();) {
					String atomName = (String) atomIter.next();
					atomName = atomName.replace('[', '_').replace(']', '_');
					alloyFunction.append(atomName);
					if (atomIter.hasNext())
						alloyFunction.append(", ");
				}
				alloyFunction.append(": " + sigName);
				if (basicTypeIter.hasNext())
					alloyFunction.append(", ");
			}
		}
		alloyFunction.append(" | { \n");

		for (Iterator sigIter = instance_.allSigs().iterator(); sigIter.hasNext();) {
			String sigName = (String) sigIter.next();
			for (Iterator fieldIter = instance_.fieldsOfSig(sigName).entrySet().iterator(); fieldIter.hasNext();) {
				Map.Entry fieldEntry = (Map.Entry) fieldIter.next();
				String fieldName = sigName + "$"
						+ ((String) fieldEntry.getKey());
				List tuples = instance_.tuplesOfRelation(fieldName);
				if (tuples.isEmpty())
					alloyFunction.append("no " + fieldName);
				else {
					alloyFunction.append(fieldName + " = ");
					for (Iterator tupleIter = tuples.iterator(); tupleIter.hasNext();) {
						String[] tupleAtomNames = (String[]) tupleIter.next();
						for (int i = 0; i < tupleAtomNames.length; i++) {
							if (i > 0)
								alloyFunction.append(" -> ");
							String atomName = tupleAtomNames[i];
							atomName = atomName.replace('[', '_').replace(']', '_');
							alloyFunction.append(atomName);
						}
						if (tupleIter.hasNext())
							alloyFunction.append(" + ");
					}
				}
				alloyFunction.append("\n");
			}
		}

		alloyFunction.append("} }");
		return alloyFunction.toString();
	}

    /**
	 * Write out the given Formula to an XML file.
	 * 
	 * @param nodeAnnotator_
	 *            optional user-defined node annotator: for each {@link Node}
	 *            returns an attribute string to add to that node's XML
	 *            representation. May be null, then no attributes are added.
	 */
    public static void writeXML(Node n_, String fname_, alloy.util.Mapper nodeAnnotator_) {
		alloy.transl.TranslOutputXMLVisitor.writeXML(n_, fname_, nodeAnnotator_);
	}

	/** dummy main method for testing purposes */
	public static void main(String[] args) {
		try {
			if (prepareSpec(args[0])) {
				System.out.println("spec compiled successfully");
				for (Iterator cmdIter = getCommands().getCommandIter(); cmdIter.hasNext();) {
					Command cmd = (Command) cmdIter.next();
					try {
						System.out.println(analyzeCommand(translateCommand(cmd), System.currentTimeMillis(), null));
					} catch (TranslationException e_) {
						System.out.println("Could not translate command: " + e_);
					} catch (EnvFailureException efe_) {
						System.out.println("Could not analyze command: " + efe_);
					}
				}
			}
			CleanupManager.exit(0);
		} catch (Exception t) {
			Dbg.fatal("Internal error", t);
		}
	}
}

